Storm 1.5.1
Date: Fri May 1 01:04:16 2020
Command line arguments: --jani sms.3-true.jani --janiproperty Unavailability --exact floats '--general:precision' 1e-20 --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4 --engine hybrid
Current working directory: /
WARN (GeneralSettings.cpp:110): Setting the precision option with module prefix does not effect all solvers. Consider setting --precision instead of --general:precision.
Time for model input parsing: 0.010s.
WARN (model-handling.h:297): Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !5 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !5 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !1 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !2 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !3 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionDEACTIVATE !4 !TRUE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionREPAIRED !0 !FALSE that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
WARN (DdJaniModelBuilder.cpp:989): Subcomposition does not have actionINSPECT !0 that is mentioned in parallel composition.
Time for model construction: 2.172s.
--------------------------------------------------------------
Model type: Markov Automaton (symbolic)
States: 1486857 (9169 nodes)
Transitions: 2437116 (5311703 nodes)
Choices: 1486857
Reward Models: none
Variables: rows: 33 meta variables (67 DD variables), columns: 33 meta variables (67 DD variables), nondeterminism: 11 meta variables (11 DD variables)
Labels: 2
* deadlock -> 1 state(s) (68 nodes)
* init -> 1 state(s) (68 nodes)
--------------------------------------------------------------
Model checking property "Unavailability": LRAmax=? [marked] ...
Result (for initial states): 1.00000000000000155431223
Time for model checking: 9.280s.